action-rename(rainv;rtinv;a)
== Case a of
== inl(x)  inl(x)
== inr(p)  kindcase(1of(p)
== inr(p)  kindcase; a.Case rainv(a) of inl(b)  inr(<locl(b),2of(p)>) ; inr(b)  inl()
== inr(p)  kindcase; l,tg.Case rtinv(tg) of
== inr(p)  kindcase; l,tg.inl(t)  inr(<rcv(l,t),2of(p)>)
== inr(p)  kindcase; l,tg.inr(b)  inl() ) 

latex

Definitions	kindcase(k; a.f(a); l,t.g(l;t) ), 1of(t), locl(a), rcv(l,tg), 2of(t),
FDL editor aliases	action-rename